| Definitions |  x:A. B(x), P   Q, P & Q, t  T,   x. t(x), S  T, S  T, Prop, Valtype(da;k), Top, f(x)?z, if b t else f fi, true, SQType(T), {T}, false, rcv(l,tg),  b, isrcv(k), lnk(k), tag(k), isl(x), True, 2of(t), outl(x), 1of(t), sends k(v:T) on l:tagged(g,State(ds),v):dt, D realizes es. P(es), A & B, tag(e),  T, e@i. P(e), xL. P(x), f o g,  x:A. B(x), State(ds), State(ds), (state when e), sends-msgs(s;v;tg_f), x(s), P  Q, DeclaredType(ds;x),  , Unit, False, P  Q,  A, isrcv(e), lnk(e), P Q, SqStable(P), Id,  , tagged-list-messages(s;v;L) |
| Lemmas | better-sends-rule, lsrc wf, fpf-join wf, Knd wf, fpf-single wf, lnk-decl wf, Kind-deq wf, Id wf, ma-state wf, ma-valtype wf, fpf-cap wf, rcv wf, decl-type wf, assert wf, isrcv wf, ldst wf, lnk wf, tagof wf, fpf wf, IdLnk wf, fpf-cap-single-join, fpf-join-cap-sq, top wf, fpf-trivial-subtype-top, fpf-dom wf, bool wf, eqtt to assert, fpf-single-dom, Knd sq, fpf-cap-single1, id-deq wf, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, lnk-decl-cap, Id sq, bool cases, bool sq, dsys wf, possible-world wf, fair-fifo wf, world wf, es-kind wf, es-lnk wf, w-es wf, es-isrcv wf, es-E wf, subtype rel wf, squash wf, true wf, es-valtype wf, subtype rel self, deq wf, isrcv-implies, IdLnk sq, es-loc wf, list-set-type2, es-tag wf, l member wf, map-map, member map, sq stable from decidable, decidable assert, l member set, list-set-type-property, decidable cand, decidable equal IdLnk, map wf, pi1 wf, tagged-list-messages-wf2, decl-state wf, es-val wf, es-when wf, es-rcv-from wf, concat wf, sends-msgs wf, l all wf, l all map, es-rcv-kind, subtype rel list, tagged-list-messages wf, d-sub wf, d-single-sends wf |
Type, T:Type.
(State(ds)
lnk-decl(l;dt)